Make PLIC interrupt 0 (no interrupt) more robust #28776
Open
+48
−24
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
In PLIC, interrupt ID 0 is special - it is reserved for "no interrupt". The way this is implemented in `rv_plic` is by simply asking nicely for integrators to tie the interrupt ID 0 input to 0. This is suboptimal because it allows integration mistakes, and there is a dangerous `assume` for FPV - this is directly added inside `rv_plic.sv`. Unless there's some flow magic to convert this to an `assert` (I didn't see anything) then this can cause nonsensical formal results if you accidentally violate that assumption. This changes that assume to an assert so it is at least checked. I would have liked to remove the pin entirely so there is no chance of making that mistake, but that is a much bigger change that requires changing the external interface. Signed-off-by: Tim Hutt <[email protected]>
Contributor
Author
|
25 minute JG results (consistent with other runs I've done): 
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
In PLIC, interrupt ID 0 is special - it is reserved for "no interrupt". The way this is implemented in
rv_plicis by simply asking nicely for integrators to tie the interrupt ID 0 input to 0.This is suboptimal because it allows integration mistakes, and there is a dangerous
assumefor FPV - this is directly added insiderv_plic.sv. Unless there's some flow magic to convert this to anassert(I didn't see anything) then this can cause nonsensical formal results if you accidentally violate that assumption.This changes that assume to an assert so it is at least checked. I would have liked to remove the pin entirely so there is no chance of making that mistake, but that is a much bigger change that requires changing the external interface.